• ExternalSite MaxBidSite(x){(1,1)}=
•   def MaxBid(bidList,max,maxBidder)=
•       bidList>[]> (maxBidder,max)
•     | bidList>x:xs>x>(bidder,bid)> if(max>bid) then MaxBid(xs,max,maxBidder) else MaxBid(xs,bid,bidder)
•   MaxBid(x,0,0) 
• EndSite

The above defines an external site named as MaxBidSite, which has forwarded trip delay of 1 time unit and return trip delay of 1 time unit. The trip delays is the same for all the external sites defined below. The usage of the site is to publish the highest bid of a list of bid.

• ExternalSite Bidder(y){(1,1)}=
•   y>(x,id,bid)>
•   (
•     def GetBid(bidList,minBid)=
•         bidList>[]> []
•       | bidList>x:xs>x>(bid,bidvalue)>(bid,bid*10+minBid):GetBid(xs,minBid)
•       x>"nextBidList">
•      
•     GetBid([(1,[]),(2,[]),(3,[])],bid)
•   )
• EndSite

The above defines an external site named as Bidders, which maintains a list of bidders and their bids, and responds to the message nextBidList, which solicits a list of higher bids for the auctioned item.

• ExternalSite Auction(x){(1,1)}=
•   systemvar AuctionList=Buffer()
•   systemvar WinList=Buffer()
•   (
•       x>("post",item)>AuctionList.put(item)
•     | x>"getNext">AuctionList.getnb()
•     | x>("won",item)>WinList.put(item)
•   )
•   ;null
• EndSite

Auction external site maintains a list of available items and responds to post, and getNext for adding and retrieving an item from the list, respectively. It also responses to won for storing the information of winning item.

• ExternalSite Seller(x){(1,1)}=
•   systemvar a=Buffer()
•   {a.put((1, 50, 500))>>a.put((2, 70, 700))}--(id,duration,minbid)
•   (x>"postNext">a.getnb());null
• EndSite

Seller site, which maintains a list of items to be auctioned and responds to the message postNext by publishing the next available item.

• globalvar bidItemSet=Set()
• globalvar wonItemSet=Set()
• globalvar conflict=false

The above declares a list of global variables. bidItemSet contains the set of items that has bid on it but has not been sold. wonItemSet contains the set of item that has been sold.
conflict is true only when there is more then one winner for a single item.

• def posting() =
•   Seller("postNext")>a>
•   (
•      (a>null> stop)
•    | (a>(id,t,m)> Auction(("post",a))>>Rtimer(10)>>posting())
•   )

The posting expression recursively queries a given seller site for the next item available for auction x, and then posts it to the auction by calling the Auction site.

• def TimeRound(y)=
•   y>(itemId, minBid, duration)>
•   (
•     x<x<(Rtimer(duration)|Bidder(("nextBidList",itemId, minBid))>bl>MaxBidSite(bl))
•   ) def bids(x)
•   x>(itemid, duration, wname, wbid)>
•   (
•     if(duration<=0) then
•      (wname,wbid)
•     else
•      TimeRound((itemid,wbid,10))>x>
•      (
•        if (x=signal) then
•         bids((itemid, duration-10,wname,wbid))
•        else
•          x>(winnername, winnerbid)>bids((itemid, duration-10,winnername,winnerbid))
•      )
•   )
• def bidding()=
•   Auction("getNext")>x>
•   (
•     (
•       x>(itemid, duration, minValue)>bids((itemid,duration,0,0)) > (wname,wbid) > bidItemSet.add(itemid)
•       >>
•         (
•           if (wname=0) then
•            bidding()
•           else
•            Auction(("won", (wname, itemid, wbid))) >> bidItemSet.remove(itemid)>>$GUpdate({conflict=wonItemSet.add(itemid)}) >>bidding()
•         )
•      )
•       
•    |  x>null>bidding()
•   )

The bidding expression recursively queries the auction site for the next item available for auction, where an item is a 3-tuple (itemid, duration, minValue), with itemid the item identier, duration its auction duration, and minValue the starting bid. The expression then collects bids for the item in rounds from the bidders site for the duration of the auction, where each round lasts for a maximum of ten unit of time. Once the bidding ends, the Bidding expression announces the winning information in a 3-tuple (wname, itemid, wbid), with wname the winning bidder name, itemid the item identifier and wbid the winning bid before proceeding to the next item. 

posting() | bidding()

The above specifies that the posting and bidding activities are running in parallel for an auction.

#define hasbid (bidItemSet.size() > 0)

The above defines a condition named as hasbid which represents the situation where there is some items that have bid on it.

#define sold (bidItemSet.size() = 0)

The above defines a condition named as sold which represents the situation where there is no item that has bid on it.

#define conflict (conflict = true)

The above defines a condition named as conflict which represents the situation where there is more than one winner for a single item.

#assert System |= [] (hasbid -> <> sold);

The above checks that if there is some elements that has bid on it, eventually all of them are sold.

#assert System |= []! conflict;

The above checks that there will never have more than one winner for a single item.